$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} .
\\[0ex]loc(lastchange($x$;$e$)) $\sim$ loc($e$)